Does your program have an overflow error? Will it work with all inputs? How do you know for sure? Test cases are the bread and butter of resilient design, but bugs still sneak into software. What if we could prove our programs are error-free?

Boolean Satisfiability (SAT) solvers determine the ‘satisfiability’ of boolean set of equations for a set of inputs. An SMT solver Satisfiability Modulo a Theory) applies SMT to bit-vectors, strings, arrays, and more. Together, we can reduce a program and prove it is satisfiable, or provide a concrete counter-example. The implications of this are computer-aided reasoning tools for error-checking in addition to much more robust programs.

In this talk Murphy Berzish will give an overview of SAT/SMT theory and some real-world solution methods. He will also demonstrate applications of SAT/SMT solvers in theorem proving, model checking, and program verification.

There are both .pdf slides and a .mp4 recording of the talk. Code samples and spellings of terms are in the slides, consider following along with the slides.

BitTorrent: Talk (x264) | Talk (PDF)

HTTP (web browser): Talk (x264) | Talk (PDF)